Linux 下使用 Spin 配合 promela 语言进行协议的模拟分析
0X00 前言
计算机网络及通信系统的核心技术是协议分析与设计。协议分析与设计是借助计算机，在相应软件平台上对以PROMELA语言为描述手段完成的设计规范，自动地完成相应协议仿真，模拟，验证测试，从而减少协议开发过程中存在的错误，提高协议开发的效率和质量。
对于给定的一个使用PROMELA描述的协议系统，SPIN可以对其执行任意的模拟，也可以生成一个C代码程序，然后对该系统的正确性进行有效检验，并报告系统中出现的死锁，无效的循环，未定义的接受和标记不完全等情况。
补充：
SPIN 是最强大的模型检测工具之一，也是迄今为止唯一获得 ACM 软件系统奖的模型 检测工具 ，本文实验所用为 SPIN 的（ GUI）界面化工具 iSPAN,Promela 是 SPIN 的一种建 模语言
0X01 iSpin 的安装
这个软件大多数是在Linux 下使用的，如果想在 windows 下使用的话需要安装 cygwin 或者 MINGW ,这里有我的好朋友莲师傅写过了—>Windows 环境下 Spin 的安装配置,但我觉得很麻烦，不如开一个虚拟机，于是我这里就介绍在 Ubuntu 16.04 下面的安装方法.
1.下载安装包
首先找到 spin 的官网下载 Linux 下的安装包，如下图所示：
2.解压
放到 linux 下解压
tar -zxvf spin648.tar.gz
得到 Spin 文件夹
cd ./Spin/Src6.4.8
3.开始编译
然后开始编译，但是因为这里编译用到了 yacc 默认是不会安装的，于是这里还要
apt-get install bison
然后执行
make
然后当前目录下就成功生成了一个编译好的 spin ，我们执行看一下
./spin
4.安装 ispin
然后我们需要安装 ispin ，我们进入 Spin 下的 iSpin 目录，给 bash 脚本执行权限
chmod a+x install.sh
然后
sudo ./install.sh
最后进入到 Spin 目录下的 Src6.4.8 目录，使用命令
sudo cp spin /usr/bin/
5.运行
使用 ispin 命令就能启动我们的 ispin 程序，如下图所示：
0X02 模拟 AB 协议
我们使用 promela 语言可以描述一个协议系统，这里我以 AB 协议为例
1.要求
首先写出AB协议的 PROMELA描述，并验证 A获取的每一个报文至少有一次是正确的，而 B 接收的
每一个报文至多有一次是正确的。
AB 协议的状态图：
因为根据状态图， S3状态和 S1状态一致，所以将 S3状态与S1状态合并。 在该过程中， 一共有 3 种信号 a,b,Err，所以我们定义 mtype = {a,b,Err}。然后定义两个信道，用于在发送方实体 A 和接收方实体 B
进行数据传输。
chan AtoB = [1] of {mtype,byte};
chan BtoA = [1] of {mtype,byte};
主要过程为：
发送方处于 S5状态，并发送报文 a(0)（模拟出错用 Err(0)），此时处于 S4等待应答。
当接收方处于 S4并接收到报文，如果是 a(0)或者是 a(1)则转向 S1状态，并发送报文 b(1)且转到 S2状态；如果是 Err(0)则转向 S5状态，并发送报文 b(0)且转到 S4状态。
而发送方如果收到的应答是 b(0)或者是 b(1)则转向 S1状态，并发送报文 a(1)且转到 S2状态。
如果是 Err(0)则回到 S5状态，并发送报文 a(0)且转到 S4状态。
我们假设接受方目前在 S2状态并接收到报文，如果是 a(0)则转向 S3（S1），如果是 a(1)则转向 S1状态，并发送报文 b(1)且转到 S2状态；如果是 Err(0)则转向 S5状态，并发送报文 b(0)
且转到 S4状态。而我们同样假设发送方处于 S2状态并接收到报文，如果是b(0)则转向 S3（S1），如果是 b(1)则转向 S1状态，并发送报文 a(1)且转到 S2状态；如果是 Err(0)则转向 S5状态，并发送报文 a(0)
且转到 S4状态。
所以我们根据分析，能够得到： A 获取的每一个报文至少有一次是正确的，而B接受的每一个报文至多有一次是正确的。
代码如下：
mtype = {Err,a,b};
chan SenderToReceiver = [1] of {mtype,byte};
chan ReceiverToSender = [1] of {mtype,byte};
proctype A_SENDER(chan InCh, OutCh)
{
S5: if
::OutCh!a(0)
::OutCh!Err(0)
fi;
if
::InCh?Err(0)-> goto S5
::InCh?b(0)-> goto S1
::InCh?b(1)-> goto S1
fi;
S1: if
::OutCh!a(1)
::OutCh!Err(0)
fi;
if
::InCh?Err(0)-> goto S5
::InCh? b(1)-> goto S1
::InCh?b(0)-> goto S1
fi;
}
proctype B_RECEIVER(chan InCh, OutCh)
{
if
::InCh?Err(0)-> goto S5
::InCh?a(0) -> goto S1
::InCh?a(1)-> goto S1
fi;
S5: if
::OutCh!b(0)
::OutCh!Err(0)
fi;
if
::InCh?Err(0)-> goto S5
::InCh?a(0) -> goto S1
::InCh?a(1)-> goto S1
fi;
S1: if
::OutCh!b(1)
::OutCh!Err(0)
fi;
if
::InCh?Err(0)-> goto S5
::InCh?a(1)-> goto S1
::InCh?a(0)-> goto S1
fi;
}
proctype B_SENDER(chan InCh, OutCh)
{
S5: if
::OutCh!b(0)
::OutCh!Err(0)
fi;
if
::InCh?Err(0)-> goto S5
::InCh?a(0) -> goto S1
::InCh?a(1)-> goto S1
fi;
S1: if
::OutCh!b(1)
::OutCh!Err(0)
fi;
if
::InCh?Err(0)-> goto S5
::InCh?a(1)-> goto S1
::InCh?a(0)-> goto S1
fi;
}
proctype A_RECEIVER(chan InCh, OutCh)
{
if
::InCh?Err(0)-> goto S5
::InCh?b(0)-> goto S1
::InCh?b(1)-> goto S1
fi;
S5: if
::OutCh!a(0)
::OutCh!Err(0)
fi;
if
::InCh?Err(0)-> goto S5
::InCh?b(0)-> goto S1
::InCh?b(1)-> goto S1
fi;
S1: if
::OutCh!a(1)
::OutCh!Err(0)
fi;
if
::InCh?Err(0)-> goto S5
::InCh? b(1)-> goto S1
::InCh?b(0)-> goto S1
fi;
}
init
{
atomic
{
run A_SENDER(ReceiverToSender,SenderToReceiver);
run B_RECEIVER(SenderToReceiver, ReceiverToSender);
}
/* atomic
{
run B_SENDER(ReceiverToSender,SenderToReceiver);
run A_RECEIVER(SenderToReceiver, ReceiverToSender);
}*/
}
我们将其保存为 AB.pml 然后使用 ispin 进行模拟
我们首先用这个工具打开 AB.pml 文件，如图所示：
点击顶部第二行中的 Syntax Check 按钮进行语法检测
如图所示：
可以看到我们的代码没有语法问题，这个时候我们就能开始模拟了
如下图所示：
0X03 模拟停止等待协议
1.基本原理
全双工通信的双方既是发送方也是接收方。为了讨论方便，仅考虑A发送数据而B接收数据并发送确认。A叫发送方，B 叫接收方。“停止等待”就是每发送完一个分组就停止发送，等待对方的确认。在收到确认后再发送下一个分组。
(1)无差错情况
A发送分组M1，发送完后就暂停发送，等待B的确认。B 收到M1后就向A 发送确认。A 在收到对M1的确认后，就继续发送下一个分组M2。同样，在收到B 对M2的确认后，再继续发送下一个分组。
(2)出现差错
A 只要超过一段时间后仍没有收到确认，就认为刚发送的分组丢失，因而重传前面发送过的分组。实现这个功能应该保证：
a)A 在发送完一个分组后，必须暂时保留已发送的分组的副本。只有在收到相应的确认后才能清除暂时保留的分组副本。
b)分组和确认分组都 必须进行编号。
c)超时计时器设置的重传时间应当比数据在分组传输的平均往返时间更长一些。
(3)确认丢失和确认迟到
假设当B发送的对M2确认丢失后，A 在设定的超时重传时间内没有收到M2的确认，但并不知道是自己发送的分组出错、丢失，或者B发送的确认丢失。因此 A 在超时计时器到期后就要重传分组M2。B在收到M2后应采取的两个动作：
a)丢弃这个重复的分组M2。
b)向A 发送确认。
这种可靠传输协议称为自动重传请求ARQ（Automatic Repeat reQuest）,可以在不可靠的传输网络上实现可靠的通信。
2.实例代码:
/*!表示发给通道头尾部,?表示从通道头部取数据*/
#define MAXSEQ 2
mtype={Msg,Ack,Nak,Err,Miss};/*类型*/
chan SenderToReceiver=[1]of{mtype,byte,byte};/*通道*/
chan ReceiverToSender=[1]of{mtype,byte,byte};
proctype SENDER(chan InCh,OutCh)/*进程说明*/
{
byte SendData;
byte SendSeq;
byte ReceivedSeq;
SendData=MAXSEQ-1;
do
::SendData=(SendData+1)%MAXSEQ;
again:
if
::OutCh!Msg(SendData,SendSeq)/*随机选择发送*/
::OutCh!Err(0,0)
::OutCh!Miss(0,0)
fi;
if
::timeout -> goto again
::InCh?Miss(0,0)-> goto again
::InCh?Err(0,0)-> goto again
::InCh?Nak(ReceivedSeq,0)->
end1: goto again
::InCh?Ack(ReceivedSeq,0)->//如果是ACK
if
::(ReceivedSeq==SendSeq)-> goto progress //如果是 seq 正确
::(ReceivedSeq!=SendSeq)-> // seq 错误
end2: goto again
fi;
fi;
progress:SendSeq=1-SendSeq;
od;
}
proctype RECEIVER(chan InCh,OutCh)
{
byte ReceivedData;
byte ReceivedSeq;
byte ExpectedData;
byte ExpectedSeq;
do
::InCh?Msg(ReceivedData,ReceivedSeq)->
if
::(ReceivedSeq==ExpectedSeq)->
progress: ExpectedSeq=1-ExpectedSeq;
if
::OutCh!Miss(0,0)
ExpectedSeq=1-ExpectedSeq;
::OutCh!Ack(ReceivedSeq,0)
::OutCh!Err(0,0)
ExpectedSeq=1-ExpectedSeq;
fi;
::(ReceivedSeq!=ExpectedSeq)
if
::OutCh!Nak(ReceivedSeq,0)
::OutCh!Err(0,0)
::OutCh!Miss(0,0)
fi;
fi;
::InCh?Err(0,0)
if
::OutCh!Nak(ReceivedSeq,0)
::OutCh!Err(0,0)
::OutCh!Miss(0,0)
fi;
::InCh?Miss(0,0)->skip;
od;
}
init/*初始进程*/
{
atomic
{
run SENDER(ReceiverToSender,SenderToReceiver);/*创建进程实例*/
run RECEIVER(SenderToReceiver,ReceiverToSender);
}
}
3.运行效果
0X04 GO-BACK-N协议
1.基本原理
网络: Go-back-N策略的基本原理：当接收方检测出时序的信息后，要求发送方重发最后一个正确接受的信息帧之后的所有未被确认的帧；或者当发送方发送了n个帧后，若发现该n帧的前一帧在计时器超时区间内仍未返回其确认信息，则该帧被判定为出错或丢失，此时发送方不得不重新发送该出错帧及其后的n帧。
你：说人话！
我： 好好好，实际上这个协议可以认为是上面我说的那个停止等待协议的一个演进版本，停止等待协议是因为我们接收方的接受速度不一定能赶上传输方的传输速度，或者是会出现一些丢包和错误的问题的解决办法，我们设置了一个确认包，要求只有在接收方发出来确认包的时候发送方才能继续发送下一帧数据，但是你有没有发现这样做效率很低，发送方那个急啊……要一直等着。
那么有没有什么方法能提高一点发送放的效率呢？这就是 GO-BACK-N 的目的，我们要让发送方在接收方没啥反应的时候接着工作，那么我们就需要一个存储多个数据帧的空间，我们形象地称之为 “窗口” ，那么我假设窗口的大小为4
（1）如果接收方没有任何反应，发送方会已知发送四个数据，到这个窗口填满为止
（2）如果接收方在发送方传输完第二个数据以后给了第一个数据的ACK回应，那么第一个数据就从这个窗口中移除，第二个数据移动到第一个数据的为止，现在窗口中就只有第二个数据
（3）如果接收方给出的回应是错误回应，表示发送中出现错误，那么整个窗口中的数据都会被清空，所有的数据重新发送
2.实例代码：
#define WIN 4 /*定义窗口大小*/
#define MAX 25/*定义发送报文计数最大值*/
chan s_r=[10] of {mtype,byte,byte};/*定义发送端到接收端传输通道*/
chan r_s=[10] of {mtype,byte,byte};/*定义接收端到发送端传输通道*/
mtype={mesg, ack, err};/*定义消息类型*/
proctype udt_sender() /*发送端进程*/
{
byte s,r,swl;/*s 为要发送的报文的序号,r 为确认报文的序号,swl 为滑动窗口下限*/
swl = 0; /*窗口初始化*/
do::swl = swl;
progress:s = swl; /*将要发送报文指针移到窗口头*/
progress1: if
::s_r!mesg(0,s)-> /*成功发送正确报文*/
(swl<=s)->s = (s+1)%MAX;/*s 后移*/
if
::goto progress1; /*在窗口内连续发送*/
::skip/*也可以不发送*/
fi;
::s_r!err(s,0) -> /*发送的报文在传输通道中出错*/
(swl<=s)->s = (s+1)%MAX;
if
::goto progress1;
::skip
fi;
::skip -> /*报文在传输通道中丢失*/
(swl<=s)->s = (s+1)%MAX;
if
::goto progress1;
::skip
fi;
fi;
if
::timeout -> goto progress /*超时,从超时报文开始重发*/
::r_s?err(0,r) -> skip /*收到错误报文不工作*/
::r_s?ack(r,0) ->/*收到正确应答报文*/
if
::(r<swl)->skip /*确认序号低于窗口下限*/
::(r>s) -> skip /*高于已发送报文最大值*/
::(swl<=r<=s) -> /*正确确认*/
swl = r;/*移动窗口*/
goto progress; /*继续发送*/
fi;
fi;
od
}
proctype udt_receiver()/*接收端进程*/
{
byte t,es;/*t 为接收报文的序号,es 为期望收到的报文序号*/
es = 0; /*初始化*/
do
::s_r?mesg(0,t) ->/*收到正确报文*/
if
::(t==es)-> /*收到报文为所期望报文*/
progress2:es = (es + 1)%MAX;/*更新期望值*/
if
::r_s!ack(es,0) /*发送确认*/
::r_s!err(0,es) /*发送的确认报文在传输通道中出错*/
::skip /*确认报文在传输通道中丢失*/
fi
::(t!=es)->/*收到无效报文*/
if
::r_s!ack(es,0)/*重发确认*/
::r_s!err(0,es) /*发送的确认报文在传输通道中出错*/
::skip /*确认报文在传输通道中丢失*/
fi
fi
::s_r?err(t,0)->/*收到的报文出错*/
if
::r_s!ack(es,0)/*重发确认*/
::r_s!err(0,es) /*发送的确认报文在传输通道中出错*/
::skip /*确认报文在传输通道中丢失*/
fi
od
}
init
{ /*启动进程*/
run udt_sender();
run udt_receiver();
}
3.运行结果
其实从这个效果图中我们也能非常清楚地看到接收方连续地接受了发送方的四个数据
0X05 总结
配合promela 语言 spin 这个工具还是非常好的模拟了协议的抽象运行过程。这门语言由于和一般的编程语言没什么关联还是要好好学一下才行，官网在这里.